Updated

I prepared this branch to merge my parallel trace abstraction approach into main.
Feel free to take a look already, make suggestions, and ideally tell me how you want it to be refactored.
Unfortunately my changes affects quite a few classes.

Before merging, I need to run a few more experiments to ensure there are no unwanted side effects.

The following changes have been made:

• ParallelNwaCegarLoop.java
  Contains the main CEGAR loop

• CegarNwaWorkerThread.java
  Is the corresponding class that does the trace check, interpolation, and generalization of the resulting automaton

• Some changes are made to the refinement strategy stuff. In the CegarNwaWorkerThread.java I can for example
  (se commented code) decide to do LoopAcceleration after seeing a PathProgram 7 times.

• IsEmptyParallel
  The search now searches for a Prefix of a counterexamples that is different from all counterexamples in a Set given as parameter. Then IsEmptyHeuristic is called with waypoints. Those waypoints are the Prefix and the IsEmptyHeuristic search follows those waypoints and after the last waypoints it searches for an accepting state.
  It will not backtrack beyond the last waypoint.

• TransferBetweenMainAndWorker
  This is now the more elegant solution to our script problem. Each worker has one such transfer class and it manages all transfers in both direction. It transfers the CfgSmtToolkit, Automata, Counterexamples. To be precise, transformulas, IProgramVars everything that the CFGSmtToolkit touches

• Wintesses
  To create a violation witness i need the sort of a value in the TypeSortTranslator. This sorts come from worker smtcfgtoolkit scripts. Since the TypeSortTranslator is created at the very start when translating to Boogie. I need a way to tell the TypeSortTranslator what the script is, that created this sort. I do this by passing it through the programexecution